System F

System Fの概要

System Fは、型付きラムダ計算の一形態であり、特に全称量化を取り入れた点が特徴です。この体系は、単純型付きラムダ計算において関数の型に関する変数とその束縛を追加し、ポリモーフィックな性質を持つように設計されています。通常、System Fは「二階ラムダ計算」や「ポリモーフィックラムダ計算」とも称されます。

このシステムは、主にプログラミング言語の型システムにおいて重要な役割を果たしており、特に関数型プログラミング言語であるMLやHaskellの基盤理論となっています。System Fは、論理学者のジャン＝イヴ・ジラールと計算機科学者のジョン・C・レイノルズによって独自に発見され、その名は偶然の命名であるとジラールは述べています。

型の変数と束縛

単純型付きラムダ計算は、主に関数の変数に焦点を当てていますが、System Fでは型にも変数と束縛が組み込まれ、より複雑で強力な表現ができるようになっています。たとえば、恒等関数は任意の型Aに対してA → Aの形で表現されますが、System Fを用いることで次のような判断が成り立つことにより、その型を示すことができます。

```
⊢ Λ α . λ xα . x : ∀ α . α → α
```

ここでのαは型変数を示し、小文字のλは通常の値に関する抽象化を示し、大文字のΛは型のレベルでの抽象化を表しています。

強正規化性と型推論の決定不能性

項書換え系としてのSystem Fは、「強正規化性」を持っており、これはあるプログラムが必ず規定の形に収束することを意味します。しかし、System Fにおける型推論のプロセスには決定不能性があるため、すべての型が自動的に推論可能ではないことに留意が必要です。この特性は、システムの使いやすさや開発者にとって重要なエンジニアリング上の課題を引き起こします。

カリー＝ハワード同型との関連性

また、System Fはカリー＝ハワード同型の原則に基づき、全称量化のみを利用した二階直観主義論理の断片と一致することも示されています。このため、System Fは依存型を含むより強力なラムダ計算の一部として、さらなる発展の基礎となるものと見なされています。

ラムダ・キューブの一部

最後に、System Fは「ラムダ・キューブ」と呼ばれる理論体系の一角を成しており、異なる型システムや計算モデルがどのように関連し合っているのかを理解する上で重要な位置づけを持っています。このことは、計算機科学やプログラミング言語の進化における鍵となる要素の一つです。

参考文献

1. Girard, Jean-Yves (1971). “Une Extension de l'Interpretation de Gödel à l'Analyse, et son Application à l'Élimination des Coupures dans l'Analyse et la Théorie des Types”. Proceedings of the Second Scandinavian Logic Symposium. Amsterdam. pp. 63–92.
2. Reynolds, John (1974). “Towards a Theory of Type Structure” (PDF). Colloque sur la Programmation. Paris, France. pp. 408–425.
3. Girard, Jean-Yves; Lafont, Yves; Taylor, Paul (1989). Proofs and Types. Cambridge University Press. ISBN 0-521-37181-3. http://www.PaulTaylor.EU/stable/Proofs%2BTypes.html
4. Wells, J. B. (1995). “Typability and type checking in the second-order lambda-calculus are equivalent and undecidable”. Proceedings of the 9th Annual IEEE Symposium on Logic in Computer Science (LICS). pp. 176–185.

もう一度検索